Dependent lenses are dependent optics

Abstract: Mixed optics and F-lenses are orthogonal generalizations of lenses, an unreasonably effective abstraction for bidirectional processes in cartesian categories. Mixed optics generalize lenses by dropping the cartesianity assumption, which makes them somehow 'linearly typed'. Instead, F-lenses generalize lenses by making them dependently typed. Both generalizations greatly improve expressivity and come with compelling examples. Therefore, it is natural to wonder whether 'dependent mixed optics', generalizing both, are a thing. In the last six months a quick succession of papers (by MSP, Milewski, Vertechi and C.) converged to a common definition. In this talk I'll review the state of the art on dependent optics, with the concrete goal of explaining Vertechi's proof that dependent lenses (aka morphisms in Poly) are dependent optics.

category theory

Audience: researchers in the topic

( slides | video )

Intercats: Seminar on Categorical Interaction